Issue2067.agda:15,9-10
Nat !=< M.A (m + 1)
when checking that the expression m has type M.A (m + 1)
